Example 5 in [Duran, Lucas, Marché, Meseguer & Urbain - PEPM'04]

Summary: Ex5_DLMMU04

• TPDB format
• OBJ format
• Negative results:
  1. Lucas'
• Positive results:
  1. CSDP
  2. Polynomial interpretation
  3. Giesl and Middeldorp's transformation

Ex5_DLMMU04 in TPDB format ( Ex5_DLMMU04.trs):

(VAR X XS N Y YS)
(STRATEGY CONTEXTSENSITIVE 
  (pairNs)
  (cons 1)
  (0)
  (incr 1)
  (oddNs)
  (s 1)
  (take 1 2)
  (nil)
  (zip 1 2)
  (pair 1 2)
  (tail 1)
  (repItems 1)
)
(RULES 
pairNs -> cons(0,incr(oddNs))
oddNs -> incr(pairNs)
incr(cons(X,XS)) -> cons(s(X),incr(XS))
take(0,XS) -> nil
take(s(N),cons(X,XS)) -> cons(X,take(N,XS))
zip(nil,XS) -> nil
zip(X,nil) -> nil
zip(cons(X,XS),cons(Y,YS)) -> cons(pair(X,Y),zip(XS,YS))
tail(cons(X,XS)) -> XS
repItems(nil) -> nil
repItems(cons(X,XS)) -> cons(X,cons(X,repItems(XS)))
)

The CS-TRS in OBJ format (file Ex4_DLMMU04.obj):

obj Ex5_DLMMU04 is
  sort S .
  op pairNs : -> S .
  op cons : S S -> S [strat (1 0)] .
  op 0 : -> S .
  op incr : S -> S .
  op oddNs : -> S .
  op s : S -> S .
  op take : S S -> S .
  op nil : -> S .
  op zip : S S -> S .
  op pair : S S -> S .
  op tail : S -> S .
  op repItems : S -> S .
  vars X XS N Y YS : S .
  eq pairNs = cons(0,incr(oddNs)) .
  eq oddNs = incr(pairNs) .
  eq incr(cons(X,XS)) = cons(s(X),incr(XS)) .
  eq take(0,XS) = nil .
  eq take(s(N),cons(X,XS)) = cons(X,take(N,XS)) .
  eq zip(nil,XS) = nil .
  eq zip(X,nil) = nil .
  eq zip(cons(X,XS),cons(Y,YS)) = cons(pair(X,Y),zip(XS,YS)) .
  eq tail(cons(X,XS)) = XS .
  eq repItems(nil) = nil .
  eq repItems(cons(X,XS)) = cons(X,cons(X,repItems(XS))) .
endo

Negative results

1. The µ-termination of Ex5_DLMMU04 cannot be proved by using Lucas' transformation. The TRS Ex5_DLMMU04_L:

   pairNs -> cons(0)
   oddNs -> incr(pairNs)
   incr(cons(X)) -> cons(s(X))
   take(0,XS) -> nil
   take(s(N),cons(X)) -> cons(X)
   zip(nil,XS) -> nil
   zip(X,nil) -> nil
   zip(cons(X),cons(Y)) -> cons(pair(X,Y))
   tail(cons(X)) -> XS
   repItems(nil) -> nil
   repItems(cons(X)) -> cons(X)
   
   

   contains extra variables.
   
2. The µ-termination of Ex5_DLMMU04 cannot be proved by using Zantema' transformation (non-terminating)(AProVE).

Positive results

1. The µ-termination of Ex5_DLMMU04 can be proved by using CSDP (computed with MuTerm).
   
2. The µ-termination of Ex5_DLMMU04 can also be proved by using a polynomial interpretation (computed with MuTerm).
   
3. The µ-termination of Ex5_DLMMU04 can also be proved by using Giesl and Middeldorp's transformation. The TRS Ex5_DLMMU04_GM:

    a__pairNs -> cons(0,incr(oddNs))
   a__oddNs -> a__incr(a__pairNs)
   a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
   a__take(0,XS) -> nil
   a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS))
   a__zip(nil,XS) -> nil
   a__zip(X,nil) -> nil
   a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS))
   a__tail(cons(X,XS)) -> mark(XS)
   a__repItems(nil) -> nil
   a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS)))
   mark(pairNs) -> a__pairNs
   mark(incr(X)) -> a__incr(mark(X))
   mark(oddNs) -> a__oddNs
   mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
   mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2))
   mark(tail(X)) -> a__tail(mark(X))
   mark(repItems(X)) -> a__repItems(mark(X))
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(0) -> 0
   mark(s(X)) -> s(mark(X))
   mark(nil) -> nil
   mark(pair(X1,X2)) -> pair(mark(X1),mark(X2))
   a__pairNs -> pairNs
   a__incr(X) -> incr(X)
   a__oddNs -> oddNs
   a__take(X1,X2) -> take(X1,X2)
   a__zip(X1,X2) -> zip(X1,X2)
   a__tail(X) -> tail(X)
   a__repItems(X) -> repItems(X)
   
   

   can be proved terminating by AProVE